Inference at * 1 1 
Iof proof for Lemma sub functionality wrt le:



1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1  j1
6. i2  j2 
  (i1+(-i2))  (j1+(-j2)) 

latex

 by ((Backchain ``add_functionality_wrt_le minus_functionality_wrt_le``) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, P  Q, x:A. B(x)
Lemmas	minus functionality wrt le, add functionality wrt le